A category is confluent if for any span , there exists a cospan . Note that we do not require the resulting square to commute.
If the morphisms in a category represent (sequences of) “rewriting” operations, then confluence means that any two ways to rewrite the same thing can eventually be brought back together.
If is an abstract rewriting system ie. a set equipped with a binary relation and if is the reflexive-transitive closure of , then we say that is confluent iff for every such that and , there exists such that and .
This is a good property of rewriting in systems such as the lambda calculus (the Church-Rosser theorem), and as such it is a property one might expect for the hom-categories in a 2-categorical model of lambda calculus.
Another good property one might want to assume is termination, i.e. the lack of infinite chains of nonidentity arrows.
As stated in the definition, the notion of confluence is perfectly sensible if we replace “category” by “directed graph (quiver)”. However, it is also occasionally useful to strengthen the notion of confluence so that commutativity of the resulting square holds in the category. An example is Mac Lane’s proof of the coherence theorem for monoidal categories (as given in Categories Work), where the “rewrite” arrows are expanded (whiskered) instances of associativity morphisms (as opposed to their inverses) in a free monoidal category.
John Baez, 2-categories of computation.
Barnaby P. Hilken, Towards a proof theory of rewriting: the simply-typed 2λ-calculus, Theor. Comp. Sci. 170 (1996), 407-444.
Last revised on March 18, 2024 at 15:38:58. See the history of this page for a list of all contributions to it.